normal{-}da\{i:l\}(${\it da}$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$fpf{-}all(Knd; KindDeq; ${\it da}$; $x$,$A$.normal{-}type\{i:l\}($A$))